__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
AND(tt, X) → ACTIVATE(X)
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
AND(tt, X) → ACTIVATE(X)
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
__1(__(X, Y), Z) → __1(Y, Z)
Used ordering: Polynomial interpretation [25,35]:
__1(__(X, Y), Z) → __1(X, __(Y, Z))
The value of delta used in the strict ordering is 1/8.
POL(__(x1, x2)) = 1/4 + x_1 + x_2
POL(__1(x1, x2)) = (1/2)x_1 + (1/2)x_2
POL(nil) = 0
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
__1(__(X, Y), Z) → __1(X, __(Y, Z))
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
__1(__(X, Y), Z) → __1(X, __(Y, Z))
The value of delta used in the strict ordering is 1/16.
POL(__(x1, x2)) = 1/4 + (4)x_1 + x_2
POL(__1(x1, x2)) = (1/4)x_1
POL(nil) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
and(tt, X) → activate(X)
isNePal(__(I, __(P, I))) → tt
activate(X) → X